(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


(** ** Matrix Addition Properties *)
Require Export List.
Require Export Matrix.Mat.Matrix_Module.
Require Import Matrix.MMat.MMat_def.
Require Import Matrix.MMat.Mlist_function.
Import ListNotations.

(* ################################################################# *)
Section MMadd.
Variable A:Set.
Variable Zero:A.
Variable add:A->A->A.
Variable sub:A->A->A.
Variable opp: A->A.
Variable m n :nat.



Section MMadd_validation.
Variable f:A->A->A.
Variable f1:A->A.
Definition Mf1:= @Mf A m n f.
Definition Mm1:= @Mm A m n f1.


Variable ma mb mc md:@Mat A m n.
Definition mm1 := mkMat_1_2 ma mb.
Definition mm1' := mkMat_1_2  mc md.
Definition mm2 := mkMat_1_2
  (matrix_each A f ma mc) (matrix_each A f mb md).

Lemma mmatrix_each_eq: 
  (matrix_each (@Mat A m n) Mf1 mm1 mm1')
  == mm2.
Proof.
  unfold mm1,mm1',mm2,matrix_each,mat_each,MM_eq.
  simpl. induction ma,mb,mc,md. unfold Mf,MMat_def.Mf.
  unfold matrix_each,mat_each,M_eq.
  simpl. auto.
Qed.

Definition mm3 := mkMat_2_1 ma mb.
Definition mm3' := mkMat_2_1 mc md.
Definition mm4 := mkMat_2_1
  (matrix_each A f ma mc) (matrix_each A f mb md).

Lemma mmatrix_each_eq2:
  (matrix_each (@Mat A m n) Mf1 mm3 mm3') 
  == mm4.
Proof.
  unfold mm1,mm1',mm2,matrix_each,mat_each,MM_eq.
  simpl. induction ma,mb,mc,md. unfold Mf,MMat_def.Mf.
  unfold matrix_each,mat_each,M_eq.
  simpl. auto.
Qed.

Variable m2 n2: nat.
Variable me : Mat (Mat A m n) m2 n2.
Variable mf : Mat (Mat A m n) m2 n2.

Lemma MMf_eq_Mf: 
  (forall a,f a Zero = a)->
  MM_to_M (matrix_each (Mat A m n) (matrix_each A f) me mf) 
  === matrix_each A f (MM_to_M me) (MM_to_M mf).
Proof.
  intros.
  unfold MM_to_M,MM_to_M',M_eq.
  unfold matrix_each,mat_each.
  simpl. induction me,mf. simpl.
  rewrite <-dlM_to_M1_mat_each' with(Zero:=Zero)(m2:=m2)(n2:=n2).
  auto. auto. auto.
  auto. auto. auto.
Qed.

Lemma MMm_eq_Mm:
  MM_to_M (matrix_map (Mat A m n) (matrix_map A f1) me)
  === matrix_map A f1 (MM_to_M me).
Proof.
  intros.
  unfold MM_to_M,MM_to_M',M_eq.
  unfold matrix_map,matrix_map'.
  simpl. induction me,mf. simpl.
  rewrite <- dlM_to_M1_dlist_map.
  auto.
Qed.


End MMadd_validation.

Section add_lemma.

Variable m2 n2:nat.
Lemma mmatrix_each_comm: forall (ma mb: Mat(Mat A m n) m2 n2),
  (forall a : A, add a Zero = a) ->
  (forall a b : A, add a b = add b a) ->
  matrix_each (Mat A m n) (matrix_each A add) ma mb 
  == matrix_each (Mat A m n) (matrix_each A add) mb ma.
Proof.
  intros. apply MM_to_M_M_eq.
  rewrite ?MMf_eq_Mf. apply matrix_comm. 
  auto. auto. auto.
Qed.

Lemma mmatrix_assoc: forall (ma mb mc: Mat(Mat A m n) m2 n2),
  (forall a : A, add a Zero = a) ->
  (forall a b c: A, add (add a b) c = add a (add b c)) ->
  matrix_each (Mat A m n) (matrix_each A add)
  (matrix_each (Mat A m n) (matrix_each A add) ma mb) mc 
  == 
  matrix_each (Mat A m n) (matrix_each A add) ma 
  (matrix_each (Mat A m n) (matrix_each A add) mb mc).
Proof.
  intros. apply MM_to_M_M_eq.
  rewrite ?MMf_eq_Mf. apply matrix_assoc. 
  auto. auto. auto. auto. auto.
Qed. 

Lemma mmatrix_add_zero_l: forall (ma: Mat(Mat A m n) m2 n2),
  (forall a : A, add a Zero = a) ->
  (forall a : A, add Zero a = a) ->
  matrix_each (Mat A m n) 
  (matrix_each A add) (MO (Mat A m n) (MO A Zero m n) m2 n2) ma == ma.
Proof.
  intros. apply MM_to_M_M_eq.
  rewrite ?MMf_eq_Mf.
  rewrite MM_to_M_MO.
  apply matrix_add_zero_l. 
  auto. auto.
Qed.

Lemma mmatrix_add_zero_r: forall (ma: Mat(Mat A m n) m2 n2),
  (forall a : A, add a Zero = a) ->
  matrix_each (Mat A m n) (matrix_each A add) ma (MO (Mat A m n) (MO A Zero m n) m2 n2) 
  == ma.
Proof.
  intros. apply MM_to_M_M_eq.
  rewrite ?MMf_eq_Mf.
  rewrite MM_to_M_MO.
  apply matrix_add_zero_r. 
  auto. auto.
Qed.

End add_lemma.

Section sub_lemma.

Variable m2 n2:nat.

Lemma mmatrix_sub_opp: forall (ma mb mc: Mat(Mat A m n) m2 n2),
  (forall a : A, sub a Zero = a) ->
  (forall a b : A, sub a b = opp (sub b a)) ->
  matrix_each (Mat A m n) (matrix_each A sub) ma mb 
  == matrix_map (Mat A m n) (matrix_map A opp) 
    (matrix_each (Mat A m n) (matrix_each A sub) mb ma).
Proof.
  intros. apply MM_to_M_M_eq.
  rewrite ?MMf_eq_Mf. rewrite MMm_eq_Mm.
  rewrite MM_to_M_matrix_each.
  apply matrix_sub_opp. auto. auto. auto. auto.
Qed.

Lemma mmatrix_sub_assoc: forall (ma mb mc: Mat(Mat A m n) m2 n2),
  (forall a : A, add a Zero = a) ->
  (forall a : A, sub a Zero = a) ->
  (forall a b c , sub (sub a b) c = sub a (add b c)) ->
  matrix_each (Mat A m n) (matrix_each A sub)
  (matrix_each (Mat A m n) (matrix_each A sub) ma mb) mc ==
  matrix_each (Mat A m n) (matrix_each A sub)
  ma (matrix_each (Mat A m n) (matrix_each A add) mb mc).
Proof.
  intros. apply MM_to_M_M_eq.
  rewrite ?MMf_eq_Mf. apply matrix_sub_assoc. 
  auto. auto. auto. auto. auto.
Qed.

Lemma mmatrix_sub_zero_l: forall (ma : Mat(Mat A m n) m2 n2),
  (forall a : A, sub a Zero = a) ->
  (forall a : A, sub Zero a = opp a) ->
  matrix_each (Mat A m n) (matrix_each A sub) 
  (MO (Mat A m n) (MO A Zero m n) m2 n2) ma 
  == matrix_map (Mat A m n) (matrix_map A opp) ma.
Proof.
  intros. apply MM_to_M_M_eq.
  rewrite ?MMf_eq_Mf. rewrite MMm_eq_Mm.
  rewrite MM_to_M_MO. apply matrix_sub_zero_l. auto.
  auto. auto.
Qed.

Lemma mmatrix_sub_zero_r: forall (ma : Mat(Mat A m n) m2 n2),
   (forall a : A, sub a Zero = a) ->
  matrix_each (Mat A m n) (matrix_each A sub) 
  ma (MO (Mat A m n) (MO A Zero m n) m2 n2)  
  == ma.
Proof.
  intros. apply MM_to_M_M_eq.
  rewrite ?MMf_eq_Mf.
  rewrite MM_to_M_MO. apply matrix_sub_zero_r. auto.
  auto.
Qed.

Lemma mmatrix_sub_self: forall (ma : Mat(Mat A m n) m2 n2),
  (forall a : A, sub a Zero = a) ->
  (forall a: A ,sub a a = Zero ) ->
  matrix_each (Mat A m n) (matrix_each A sub) 
  ma ma 
  == (MO (Mat A m n) (MO A Zero m n) m2 n2) .
Proof.
  intros. apply MM_to_M_M_eq.
  rewrite ?MMf_eq_Mf.
  rewrite MM_to_M_MO. apply matrix_sub_self. auto.
  auto.
Qed.

End sub_lemma.


End MMadd.

